
/* Bidder1 States */

mtype = { idleB, startB, submittedB };

/* Auctioneer States */

mtype ={ waitA, startA, processBidA, endA };

/* Events*/

mtype = { start_auction, auction_started, status, winner, end_auction, dummy };

mtype stateB;
mtype stateA;
	
/* channels for transitions */	

chan m2A = [0] of { int, mtype };
chan m2B = [0] of { int, mtype };
int clientBid;
int startBid=14; 

init {
	atomic {
		if
		:: skip -> clientBid = 12;
		:: skip -> clientBid = 13;
		:: skip -> clientBid = 14;
		fi;
	}
	run auctioneer();
	m2A!0, start_auction;
	printf("Msg to start the auction\n");

}

/*Client process*/

proctype client1() {
	stateB = idleB;

	do
	:: (stateB == idleB) -> 
		printf("Client waiting for auction to start\n");
		if
		:: m2B?0, auction_started->
		printf("The auction is now open, the client knows");
		stateB = startB;
		:: m2B?0, end_auction -> printf("Auction is terminating \n");
		break;
		fi;
	:: (stateB == startB) -> 
		printf("Ready to submit a bid\n");
		printf("Sending bid %d\n",clientBid);
		m2A!clientBid, dummy;
		stateB = submittedB;
	::(stateB == submittedB) -> 
		printf("Bid submitted\n");
		printf("Waiting for the result now\n");
		if
		::m2B?0, status ->
		printf("Bid too low\n");
		stateB = idleB; 
		::m2B?0, winner->
		printf("Hurray, I won\n");
		stateB=idleB;
		fi;
	od;
}


/*Auction process*/

proctype auctioneer() {
	stateA = waitA;
	run client1();
	do
	:: (stateA == waitA) -> 
		printf("Waiting to start the auction\n");
		m2A?0, start_auction;
		printf("Ready to get the auction started\n");
		m2B!0, auction_started;
		stateA= startA;
		printf("Sending start signal\n");
	:: (stateA == startA) -> 
		printf("Waiting for a bid to be submitted....\n");
		m2A?clientBid, dummy; 
		printf("Client bid received\n");
		stateA=processBidA;
	:: (stateA == processBidA) -> printf("Computing current winner\n");
		if
		:: clientBid>startBid -> m2B!0, winner;stateA=endA;
		:: clientBid<startBid -> m2B!0, status;stateA = endA; 
		fi;
	:: (stateA == endA) -> 
		printf("Winner elected.Auction will terminate\n");
		m2B!0,end_auction;
		break;
	od;
}

